$\forall$${\it ds}$:fpf(Id; $x$.Type), ${\it da}$:fpf(Knd; $k$.Type), $x$:ecl(${\it ds}$; ${\it da}$).
\\[0ex]ecl{-}trans($x$) $\in$ ecl{-}trans{-}tuple\{i:l\}(${\it ds}$; ${\it da}$)